M:MsgA, x:Id, s1, s2:M.(timed)state. ma-x-tequiv(M;x;s1;s2)   

latex

Definitions	MsgA, t  T, Id, x:A. B(x), M.ds(x), , x:AB(x), f(a), s = t, , A, P  Q, timedState(ds), ma-x-tequiv(M;x;s1;s2), M.(timed)state
Lemmas	not wf, rationals wf, ma-ds wf, Id wf, msga wf